Termination w.r.t. Q proof of /tmp/tmpoAuZex/z008.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

The set Q is empty.
We have obtained the following QTRS:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))

Used ordering:
Polynomial interpretation [25]:

POL(a(x₁)) = 2·x₁
POL(b(x₁)) = 2·x₁
POL(s(x₁)) = 2 + 2·x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → B(a(b(x1)))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → B(a(b(x1)))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
B(a(b(b(x1)))) → B(a(b(x1)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(A(x₁)) = x₁
POL(B(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 2 + 2·x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(b(a(a(x1)))) → B(a(b(a(x1)))) at position [0] we obtained the following new rules:

A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule B(a(b(b(x1)))) → A(b(a(b(x1)))) at position [0] we obtained the following new rules:

B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ QDPToSRSProof

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The finiteness of this DP problem is implied by strong termination of a SRS due to [12].

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ QDPToSRSProof

                        ↳ QTRS

                          ↳ QTRS Reverse

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))
B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))
B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

The set Q is empty.
We have obtained the following QTRS:

b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))
b(b(a(b(b(a(B(x))))))) → b(a(b(a(a(b(A(x)))))))
a(a(b(a(a(b(A(x))))))) → a(b(a(b(b(a(B(x)))))))
a(a(a(b(A(x))))) → a(b(a(b(B(x)))))
b(b(a(a(b(A(x)))))) → b(a(b(a(a(B(x))))))
a(a(b(b(a(B(x)))))) → a(b(a(b(b(A(x))))))
b(b(b(a(B(x))))) → b(a(b(a(A(x)))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ QDPToSRSProof

                        ↳ QTRS

                          ↳ QTRS Reverse

                            ↳ QTRS

                              ↳ RFCMatchBoundsTRSProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))
b(b(a(b(b(a(B(x))))))) → b(a(b(a(a(b(A(x)))))))
a(a(b(a(a(b(A(x))))))) → a(b(a(b(b(a(B(x)))))))
a(a(a(b(A(x))))) → a(b(a(b(B(x)))))
b(b(a(a(b(A(x)))))) → b(a(b(a(a(B(x))))))
a(a(b(b(a(B(x)))))) → a(b(a(b(b(A(x))))))
b(b(b(a(B(x))))) → b(a(b(a(A(x)))))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 1. This implies Q-termination of R.
The following rules were used to construct the certificate:

b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))
b(b(a(b(b(a(B(x))))))) → b(a(b(a(a(b(A(x)))))))
a(a(b(a(a(b(A(x))))))) → a(b(a(b(b(a(B(x)))))))
a(a(a(b(A(x))))) → a(b(a(b(B(x)))))
b(b(a(a(b(A(x)))))) → b(a(b(a(a(B(x))))))
a(a(b(b(a(B(x)))))) → a(b(a(b(b(A(x))))))
b(b(b(a(B(x))))) → b(a(b(a(A(x)))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

507, 508, 511, 512, 510, 509, 514, 515, 513, 517, 516, 522, 523, 519, 520, 518, 521, 527, 528, 526, 524, 525, 529, 531, 532, 530, 533, 534, 540, 539, 536, 537, 535, 538, 543, 544, 541, 542, 548, 549, 547, 545, 546, 550

Node 507 is start node and node 508 is final node.

Those nodes are connect through the following edges:

507 to 509 labelled b_1(0)
507 to 513 labelled a_1(0)
507 to 518 labelled a_1(0)
507 to 524 labelled b_1(0)
508 to 508 labelled #_1(0)
511 to 512 labelled a_1(0)
511 to 508 labelled a_1(0)
511 to 530 labelled a_1(1)
511 to 535 labelled a_1(1)
512 to 508 labelled A_1(0)
510 to 511 labelled b_1(0)
509 to 510 labelled a_1(0)
514 to 515 labelled a_1(0)
515 to 516 labelled b_1(0)
513 to 514 labelled b_1(0)
517 to 508 labelled A_1(0)
516 to 517 labelled b_1(0)
516 to 508 labelled B_1(0)
522 to 523 labelled a_1(0)
523 to 508 labelled B_1(0)
519 to 520 labelled a_1(0)
520 to 521 labelled b_1(0)
520 to 508 labelled b_1(0)
520 to 541 labelled b_1(1)
520 to 545 labelled b_1(1)
518 to 519 labelled b_1(0)
521 to 522 labelled b_1(0)
527 to 528 labelled a_1(0)
528 to 529 labelled b_1(0)
528 to 508 labelled B_1(0)
526 to 527 labelled a_1(0)
524 to 525 labelled a_1(0)
525 to 526 labelled b_1(0)
529 to 508 labelled A_1(0)
531 to 532 labelled a_1(1)
532 to 533 labelled b_1(1)
532 to 508 labelled b_1(1)
532 to 541 labelled b_1(1)
532 to 545 labelled b_1(1)
530 to 531 labelled b_1(1)
533 to 534 labelled b_1(1)
533 to 508 labelled B_1(1)
534 to 508 labelled A_1(1)
540 to 508 labelled B_1(1)
539 to 540 labelled a_1(1)
536 to 537 labelled a_1(1)
537 to 538 labelled b_1(1)
535 to 536 labelled b_1(1)
538 to 539 labelled b_1(1)
543 to 544 labelled a_1(1)
543 to 508 labelled a_1(1)
543 to 530 labelled a_1(1)
543 to 535 labelled a_1(1)
544 to 508 labelled A_1(1)
541 to 542 labelled a_1(1)
542 to 543 labelled b_1(1)
548 to 549 labelled a_1(1)
549 to 550 labelled b_1(1)
549 to 508 labelled B_1(1)
547 to 548 labelled a_1(1)
545 to 546 labelled a_1(1)
546 to 547 labelled b_1(1)
550 to 508 labelled A_1(1)

We have reversed the following QTRS:
The set of rules R is

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

The set Q is empty.
We have obtained the following QTRS:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

    ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

Q is empty.